Rubik’s Cube in Lean

This Github repo contains the proof that there are $2^{12}\times 3^8\times 8!\times 11!$ Rubik’s cubes:

https://github.com/vihdzp/rubik-lean4

What! This is the most amazing thing I’ve read in a long time. What is the reason of this number? And it’s verified in Lean!!!